$\forall$$i$, $a$, $x$:Id, $X$:Type, $x_{0}$:$X$, $P$:($X$$\rightarrow\mathbb{B}$), $p$:FinProbSpace, ${\it es}$:ES.
\\[0ex]pre{-}init1{-}p(${\it es}$;$i$;$x$;$X$;$x_{0}$;$a$;$p$;$P$) $\in$ $\mathbb{P}$